Repository navigation
codegen: the facts' interval of an int32 local reaches the range proofs, and a key they bound to int32 is lowered as its i32 - #14453
Merged
Conversation
added 30 commits
November 11, 2026 10:13
…ot of any sign; probes # typed_call and PERRY_SIG_DIAG
…s and typed I32 parameters
# Conflicts: # crates/perry-codegen/src/expr/mod.rs # crates/perry/src/commands/compile/compile_env/tests.rs # scripts/test-verify-facts-s0.py
Pre-merge checks:
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Second PR of the typed-
setlane (on top of #14450, which typedset$sig(i32[-128,255], i32[-8,7])). The typed bodystill ran its integer work in doubles:
wpfacts proves an interval for each of
old,pieceandsquare, but exported only "this local is an int32"(
ElisionFacts::int32_inputs), and a typed body seeded only parameters whose interval starts at 0. Codegen's rangeproofs (
range_facts::int_range_expr) therefore knew nothing about a signed int32 local, so:perry_array_index_normalize_i32(a call) in the runtime-key arm;form=f64);What changes
ElisionFacts::int32_ranges, fromBindingFacts::int_range; the perry driverfills it beside
int32_inputs). No wpfacts change: the fact existed.letreads its interval (range_facts::facts_local_range): the last resort ofint_range_for_local, after every local proof (a loop fact, an alias, a constant, the parameter summary). Theinterval is whole-life (every value the local ever holds), so it needs no dominating guard. Only a
letofFnCtx::facts_int32_locals(not boxed, no module global), in a body that uses the facts.signature_entry::param_range_facts,seeded into
FnCtx::int_range_factsunder a scope no loop ends): T1'snonnegative_params, generalised to anysign. Written parameters are demoted by plan selection and seed nothing.
expr/int32_key.rs): the runtime-key elementread (
index_get) and the runtime-key store (index_set) lower such a key withlower_expr_as_i32(its i32chain, exact because the chain's result is in int32 and below 2^53 at every step) and hand it to the canonical
split as a native key. The split's unsigned bound (N10) declines a negative key onto the arm that reads the
original value, as for any native key. At-rest sites take the int32 form through the same range
(
rest_elems::int32_keyalready askedint_range_expr).Switch, probe, witness, sabotage
PERRY_FACTS_LOCAL_RANGES=0(off,false): none of the above (main's lowering). Compile-cache input(
compile_env.rs, testlocal_ranges_switch_is_a_cache_input).PERRY_REST_DIAG=1shows the at-rest forms (form=f64→form=i32/form=rep);# rep … range=inPERRY_FACTS_DUMPis the interval read.PERRY_VERIFY_FACTS=1): the store witness of a proven int32let(
facts_int32_locals::witness_exact) also tests that the stored value lies in the interval the range proofsread ("int32 input", exit 86). A typed parameter's interval is witnessed at every typed site and at the boxed
entry (P2's
witness_value, unchanged).local-range-negative(PERRY_FACTS_SABOTAGE=localrange: the interval claimed is its lower boundalone): correct rc 0, sabotaged rc 86, predicate
int32 input.Results
Chess (qb10,
instructions:uM, one build, on vsPERRY_FACTS_LOCAL_RANGES=0, twice each, identical runs,checksums and PV equal in every arm). Build y1 = c96e5d4, the PR's code on main 7523aa7 (#14450); the PR head adds the merge of main
6d3cd78, not re-measured:
Before merging main (build x2, on main e4f004e + #14450's branch): 20 466.3 / 467.5 / 1 429.9 / 678.7 vs
21 360.0 / 490.7 / 1 487.8 / 700.5 (−4.18 / −4.73 / −3.89 / −3.11%). The parts, on that base: the interval alone
(no key lowering, build x1) −1.12 / −1.22 / 0 / −0.83%; the key lowering adds the rest, and all of evaluate.
Per function, search 250000 (
perf record -e instructions:u,--debug-symbolsbuilds, M = sample share × total):make$sig(with the inlinedset$sig)unmake$sigevaluate$sigperry_array_index_normalize_i32In
set's body the Zobrist key is nowshl $7, old; lea 0x300(square, old)in place ofvaddsd; vmulsd; vaddsd; call perry_array_index_normalize_i32, and the board read iscmp $0x80, square; jae cold; loadin place of thedouble-key test. At-rest forms (
PERRY_REST_DIAG):set$sigreadform=rep, storeform=i32(off: bothform=f64);make$sig'sat(captureSquare)form=rep;unmake$sig4 of its 5 storesform=i32(off: 2).In evaluate the normalizer is no longer sampled (9.4 M off): its keys built from int32
lets are i32 chains.Peak RSS (
/usr/bin/time %M, KiB, 5 runs each, y1): search 26 880 ×5 both arms; perft 19 456 (one 19 200off); evaluate 19 456 (one 19 200 off); legal 19 456 (one 18 944 each). Equal.
Where else it engages: the parity IR census was stopped part way (owner order: no long gates): of 2 473
programs compared, 79 change IR, none of them changes output or compile rc. tssrc: no proven site lost or gained;
the three.js skin is byte-equal in every section.
Gates
qb10, on vs
PERRY_FACTS_LOCAL_RANGES=0, build y1 = c96e5d4 (the PR head's code on main 7523aa7). The PR head 2cab0e0 adds only the mergeof main 6d3cd78 (clean; 11 commits in transform, EH and JSON), not re-measured. Pre-merge builds x1 / x2 where a row says so.
PERRY_VERIFY_FACTS=1)let)local-range-negative: correct rc 0, sabotaged rc 86, predicateint32 input)PERRY_REST_ELEMS=0, verify, GC schedule stress on, stress off}number/test_facts_local_ranges(new),function/test_p2_signed_index_params(its at-rest board:form=i32/form=repon,form=f64off),test_p2_signature_methods,test_p2_signature_functions,test_rest_capacity,test_rest_loops,test_rest_elems,test_rest_fields,test_rest_zero_sign,test_n1_int_temps,test_facts_int32_bindings,test_array_reps_fields,test_array_reps_loop_base_gcPERRY_GC_SCHEDULE_SEED=7,RATE=1)test_p2_signed_index_params25 / 4 396; the others as in #14450. Output equals node in every armPERRY_VERIFY_FACTS=1facts_int32_locals::range_tests(IR):a_key_built_from_a_ranged_int32_let_is_an_i32_key,an_interval_whose_chain_leaves_int32_is_no_i32_key; perrycompile_env:local_ranges_switch_is_a_cache_inputfacts_int32_locals(with the newrange_tests): 3 passed, 0 failed (Mac, dev profile, on the head's code before merging main). perrycompile_env: not run for this PR. Full suites: not run (owner order 2026-11-11)-D warnings--lib --tests: 0 errors (Mac,cargo check). Other crates: this PR adds one field to a codegen struct and one insert in the perry driver; not runscripts/check_file_size.shexpr/mod.rsgains two lines (theint32_keymodule and one re-export): its allowlist count is set to its real count, 2 844 (it was stale on main, 2 842 vs 2 838). Every other file this PR touches is below the threshold. The script's other stale counts are main'sNot done
See FOLLOWUPS "[typed set follow-ups]":
const old = this.at(square)) still tests?? 0on adouble on the hit path;
this.hashA ^= xreads the I32 lane as a double and runs the guarded ToInt32 on it. Tellingis_known_i32_rangethat an I32 lane read and a present at-rest element read are int32 changed nothing on chess(20 465.9 vs 20 466.4 M on search), so it is not in this PR: the compound assignment takes another path;
unmake'sundo.captureSquarestore keeps the double key (a doublefield).